// ***** This file is automatically generated from FunctionBinary.java.jpp
// ***** (and files it recursively includes).

package daikon.inv.ternary.threeScalar;

import daikon.*;
import daikon.inv.*;
import daikon.inv.binary.twoScalar.*;
import daikon.inv.unary.scalar.*;
import daikon.derive.unary.*;
import daikon.suppress.*;
import plume.*;
import java.lang.reflect.*;
import java.util.*;
import java.util.logging.Logger;

/**
 * Base class for each of the FunctionBinaryFloat functions and permutatons.
 * Most of the work is done here.  The subclasses basically define the
 * function and return information describing the function and permutation
 * to these methods
 */
public abstract class FunctionBinaryFloat extends ThreeFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  /**
   * Boolean. True if FunctionBinaryFloat invariants should be considered.
   **/
  public static boolean dkconfig_enabled = false;

  public static Logger debug
    = Logger.getLogger("daikon.inv.ternary.threeScalar.#CLASSNAME");

  static final int[][] var_indices;
  static {
    var_indices = new int[7][];
    var_indices[1] = new int[] { 0, 1, 2 };
    var_indices[2] = new int[] { 1, 0, 2 };
    var_indices[3] = new int[] { 2, 0, 1 };
    var_indices[4] = new int[] { 0, 2, 1 };
    var_indices[5] = new int[] { 1, 2, 0 };
    var_indices[6] = new int[] { 2, 1, 0 };
  }

  protected FunctionBinaryFloat (PptSlice ppt) {
    super (ppt);
  }

  protected /*@Prototype*/ FunctionBinaryFloat () {
    super ();
  }

  /** returns whether or not this invariant is enabled **/
  public boolean enabled() {
    return dkconfig_enabled;
  }

  /** FunctionBinaryFloat is only valid on isFloat() types **/
  public boolean instantiate_ok (VarInfo[] vis) {

    if (!valid_types (vis))
      return (false);

    // Make sure that each variable is integral (not boolean or hashcode)
    if (!vis[0].file_rep_type.isFloat()
        || !vis[1].file_rep_type.isFloat()
        || !vis[2].file_rep_type.isFloat())
      return (false);

    return (true);
  }

  // check_modified relies on func having no side effects.
  abstract double func (double arg1, double arg2);
  abstract boolean is_symmetric();
  abstract String[] get_method_name();
  abstract int get_var_order();
  abstract void set_function_id (int function_id);
  abstract int get_function_id ();

  /**
   * Map from function name (eg, MultiplyLong, MinimumFloat) to an array
   * of instances (one for each valid permutation) for that function.
   */
  private static Map<String,/*@Prototype*/ FunctionBinaryFloat[]> functions = new LinkedHashMap<String,/*@Prototype*/ FunctionBinaryFloat[]>();

  /**
   * A list indexed by function number to an array of instances (one for
   * each valid permutation) for that function.  The array is the same
   * one as is stored in the functions Map.  This provides a faster access
   * mechanism once we have the function id (which are calculated the first
   * time through).
   */
  private static List</*@Prototype*/ FunctionBinaryFloat[]> func_list = new ArrayList</*@Prototype*/ FunctionBinaryFloat[]>();

  private static void build_func_list() {

    // Reflection seems to confuse clover
    ///CLOVER:OFF

    // Build the map of functions to array of instances for that function
    debug.fine ("Processing FunctionBinaryFloat");
    functions = new LinkedHashMap<String,/*@Prototype*/ FunctionBinaryFloat[]>();
    @SuppressWarnings("unchecked")
    Class</*@Prototype*/ FunctionBinaryFloat>[] subclasses = (Class</*@Prototype*/ FunctionBinaryFloat>[]) FunctionBinaryFloat.class.getDeclaredClasses();
    for (int ii = 0; ii < subclasses.length; ii++) {
      Class</*@Prototype*/ FunctionBinaryFloat> subc = subclasses[ii];
      String function = subc.getName();
      if (function.indexOf ("CLOVER") >= 0)
        continue;
      function = function.replaceFirst (".*FunctionBinary\\$", "");
      function = function.replaceFirst ("_.*", "");
      if (function.equals ("SubClass"))
        continue;
      /*@Prototype*/ FunctionBinaryFloat[] fb_arr = functions.get (function);
      if (fb_arr == null) {
        fb_arr = new /*@Prototype*/ FunctionBinaryFloat[7];
        functions.put (function, fb_arr);
        func_list.add (fb_arr);
      }
      int func_id = func_list.indexOf (fb_arr);
      @SuppressWarnings({"nonprototype"})
      /*@Prototype*/ FunctionBinaryFloat fb = null;
      try {
        Constructor</*@Prototype*/ FunctionBinaryFloat> con = subc.getDeclaredConstructor (new Class<?>[] {});
        fb = con.newInstance (new Object[] {});
      }  catch (Exception e) {
        throw new Error (" can't create instance for " + subc.getName()
                        + ": '" + e + "' ii = " + ii);
      }
      assert fb_arr[fb.get_var_order()] == null;
      fb_arr[fb.get_var_order()] = fb;
      fb.set_function_id (func_id);
      debug.fine ("Adding " + function + " " + fb.getClass().getName()
                  + " " + fb.get_var_order() + " " + fb.get_function_id());
    }
    ///CLOVER:ON
  }

  /**
   * Returns a list of all of the FunctionBinaryFloat prototype invariants
   */
  public static List</*@Prototype*/ Invariant> get_proto_all() {

    List</*@Prototype*/ Invariant> result = new ArrayList</*@Prototype*/ Invariant>();

    // If this is the first call
    if (functions.isEmpty()) {
      build_func_list();
    }

    // Get the proto invariant for all of the subclasses and return them
    for (/*@Prototype*/ FunctionBinaryFloat[] fb_arr : func_list) {
      for (int jj = 1; jj < fb_arr.length; jj++) {
        /*@Prototype*/ FunctionBinaryFloat fb = fb_arr[jj];
        if (fb != null) {
          result.add (fb);
        }
      }
    }
    return (result);
  }

  /** Permuted result var. */
  public VarInfo resultVar() {
    return ppt.var_infos[var_indices[get_var_order()][0]];
  }

  /** Permuted arg1 var. */
  public VarInfo argVar1() {
    return ppt.var_infos[var_indices[get_var_order()][1]];
  }

  /** Permuted arg2 var. */
  public VarInfo argVar2() {
    return ppt.var_infos[var_indices[get_var_order()][2]];
  }

  /**
   * Apply the specified sample to the function, returning the result
   * The caller is responsible for permuting the arguments.
   */
  public InvariantStatus check_ordered (double result, double arg1,
                                      double arg2, int count) {
    // This implementation relies on func having no side effects.
    try {
      if (!(Global.fuzzy.eq (result, func (arg1, arg2))))
        return InvariantStatus.FALSIFIED;
    } catch (Exception e) {
        return InvariantStatus.FALSIFIED;
    }
    return InvariantStatus.NO_CHANGE;
  }

  /**
   * Apply the specified sample to the function, returning the result
   * The caller is responsible for permuting the arguments.
   */
  public InvariantStatus add_ordered (double result, double arg1,
                                      double arg2, int count) {
    return check_ordered(result, arg1, arg2, count);
  }

  /**
   * Reorganize our already-seen state as if the variables had shifted
   * order underneath us (re-arrangement given by the permutation).
   * We accomplish this by returning the class that corresponds to the
   * the new permutation.
   */
  protected Invariant resurrect_done (int[] permutation) {

    assert permutation.length == 3;
    assert ArraysMDE.fn_is_permutation(permutation);

    int[] new_order = new int[3];
    int[] old_order = var_indices[get_var_order()];

    // "permutation" is a permutation on the var_info array. old_order
    // was the permutation that took the formatted invariant to the
    // var_info array, so old_order^-1 is the permutation from the
    // var_info array to the old formatted invariant. We want to find
    // a new_order so that when we first do "permutation", then
    // apply the new permutation from the var_info array to the
    // formatted invariant, we get the same formatted invariant.
    // What we want, then. is:
    //    new_order^-1 o permutation = old_order^-1
    // rearranging, this is equivalent to
    //    new_order = permutation o old_order
    new_order[0] = permutation[old_order[0]];
    new_order[1] = permutation[old_order[1]];
    new_order[2] = permutation[old_order[2]];

    // Force symmetric functions into a canonical form so that
    // we can match them when necessary and they always print the same.
    // For example, order of 0, 1, 2 and 0, 2, 1 represent the same
    // invariant for a symmetric function.  This forces them to always
    // be represented as 0, 1, 2
    if (is_symmetric ()) {
      if (new_order[2] < new_order[1]) {
        int tmp = new_order[2];
        new_order[2] = new_order[1];
        new_order[1] = tmp;
      }
    }

    // Look for the new order in the list of possible orders
    int var_order = -1;
    for (int i=0; i < var_indices.length; i++) {
      if (Arrays.equals(new_order, var_indices[i])) {
        var_order = i;
        break;
      }
    }
    assert var_order != -1;

    // If the var order hasn't changed, we don't need to do anything
    if (var_order == get_var_order())
      return (this);

    // Find the class that corresponds to the new order
    if (functions.isEmpty())
      build_func_list();
    int func_id = get_function_id();
    /*@Prototype*/ FunctionBinaryFloat[] fb_arr = func_list.get (func_id);
    assert fb_arr != null;
    for (int ii = 0; ii < fb_arr.length; ii++)
      if ((fb_arr[ii] != null) && (fb_arr[ii].get_var_order() == var_order))
        return (fb_arr[ii].instantiate_dyn (ppt));

    throw new Error ("Could not find new ordering");
  }

  public String repr() {
    return format();
  }

  public String format_using(OutputFormat format) {
    if (format == OutputFormat.SIMPLIFY) {
      return format_simplify();
    }

    int var_order = get_var_order();
    String[] methodname = get_method_name();

    VarInfo argresultvi = ppt.var_infos[var_indices[var_order][0]];
    VarInfo arg1vi = ppt.var_infos[var_indices[var_order][1]];
    VarInfo arg2vi = ppt.var_infos[var_indices[var_order][2]];

    String argresult_name = argresultvi.name_using(format);
    String arg1_name = arg1vi.name_using(format);
    String arg2_name = arg2vi.name_using(format);

    if (format == OutputFormat.DAIKON) {
      return argresult_name + " == (" + methodname[0] + arg1_name
        + methodname[1] + arg2_name + methodname[2] + ")";
    }

    if (format.isJavaFamily()) {
      if (methodname[1].equals(" || ") || methodname[1].equals(" && ")) {
        return "(" +  argresult_name + " != 0) == ((" + methodname[0] + arg1_name + " != 0)"
          + methodname[1] + "(" + arg2_name + methodname[2] + " != 0))";
      } else {
        return argresult_name + " == (" + methodname[0] + arg1_name
          + methodname[1] + arg2_name + methodname[2] + ")";
      }
    }

    return format_unimplemented(format);
  }

  public String format_simplify() {
    int var_order = get_var_order();
    String[] methodname = get_method_name();
    VarInfo[] vis = ppt.var_infos;

    String result = vis[var_indices[var_order][0]].simplifyFixedupName();
    String arg1 =   vis[var_indices[var_order][1]].simplifyFixedupName();
    String arg2 =   vis[var_indices[var_order][2]].simplifyFixedupName();
    String func = null;
    if (methodname[1].equals(" * ")) {
      func = "*";
    } else if (methodname[1].equals(" | ")) {
      func = "|java-bitwise-or|";
    } else if (methodname[1].equals(" || ")) {
      func = "|java-logical-or|";
    } else if (methodname[1].equals(", ")) {
      if (methodname[0].equals("java.lang.Math.min("))
        func = "min";
      else if (methodname[0].equals("java.lang.Math.max("))
        func = "max";
      else if (methodname[0].equals("plume.MathMDE.gcd("))
        func = "gcd";
      else if (methodname[0].equals("java.lang.Math.pow("))
        func = "pow";
      else if (methodname[0].equals("plume.MathMDE.logicalXor("))
        func = "|java-logical-xor|";
    } else {
      assert methodname[0].equals("");
      assert methodname[2].equals("");
      func = "|java-" + methodname[1].trim() + "|";
    }
    if (func == null)
      return "format_simplify() doesn't know function " + methodname[0] + "-" +
        methodname[1] + "-" + methodname[2];
    return "(EQ " + result + " (" + func + " " + arg1 + " " + arg2 + "))";
  }

  // If our classes match, we must match
  public boolean isSameFormula(Invariant other) {
    return true;
  }
  public double computeConfidence() {
    if (logOn()) {
      VarInfo v1 = ppt.var_infos[0];
      VarInfo v2 = ppt.var_infos[1];
      VarInfo v3 = ppt.var_infos[2];
      log("computeConfidence(" + format()
         + ": num_values = " + ppt.num_values()
         + ", num_values(" + v1.name() + ")=" + ppt.parent.num_values(v1)
         + ", num_values(" + v2.name() + ")=" + ppt.parent.num_values(v2)
         + ", num_values(" + v3.name() + ")=" + ppt.parent.num_values(v3));
    }
    return Invariant.conf_is_ge(ppt.num_values(), 5);
  }

  /**
   * If the arg is a sequence size, return the sequence; otherwise return null.
   **/
  private /*@Nullable*/ VarInfo sized_sequence(VarInfo size) {
    if (size.derived instanceof SequenceLength) {
      return ((SequenceLength)size.derived).base;
    }
    return null;
  }

  public /*@Nullable*/ DiscardInfo isObviousDynamically(VarInfo[] vis) {

    DiscardInfo super_result = super.isObviousDynamically(vis);
    if (super_result != null) {
      return super_result;
    }

    // Discard if any two of the three variables are the sizes of the
    // same arrays.
    VarInfo arr1 = sized_sequence(vis[0]);
    VarInfo arr2 = sized_sequence(vis[1]);
    VarInfo arr3 = sized_sequence(vis[2]);
    if (((arr1 != null) && (arr1 == arr2))
        || ((arr1 != null) && (arr1 == arr3))
        || ((arr2 != null) && (arr2 == arr3))) {
      return new DiscardInfo(this, DiscardCode.obvious,
                    "two are sizes of same array:  "
                    + vis[0].name() + " "
                    + vis[1].name() + " "
                    + vis[2].name());
    }

    return null;
  }

  // default is that it is not this function, overriden in the subclass
  public boolean isMultiply () {
    return (false);
  }

/**
 * Represents the invariant <samp>x = Multiply (y, z)</samp>
 * over three double scalars.
 */
public static class MultiplyDouble_xyz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ MultiplyDouble_xyz proto;

  /** Returns the prototype invariant for MultiplyDouble_xyz **/
  public static /*@Prototype*/ MultiplyDouble_xyz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ MultiplyDouble_xyz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected MultiplyDouble_xyz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new MultiplyDouble_xyz (slice);
  }

  private MultiplyDouble_xyz (PptSlice slice) {
    super (slice);
  }

  public MultiplyDouble_xyz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"", " * ", ""};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert MultiplyDouble_xyz.function_id == -1;
    MultiplyDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (true);
  }

  public double func (double y, double z) {

    return (y * z);
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (x, y, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", x, y, z));
    return (add_ordered (x, y, z, count));
  }

  public boolean isMultiply() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (MultiplyDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(0,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == 0) && (y == 0) ==> r = y * z
        new NISuppression (result_eq_0, arg1_eq_0, suppressee),

        // (r == 0) && (z == 0) ==> r = y * z
        new NISuppression (result_eq_0, arg2_eq_0, suppressee),

        // (r == y) && (z == 1) ==> r = y * z
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),

        // (r == z) && (y == 1) ==> r = y * z
        new NISuppression (result_eq_arg2, arg1_eq_1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>y = Multiply (x, z)</samp>
 * over three double scalars.
 */
public static class MultiplyDouble_yxz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ MultiplyDouble_yxz proto;

  /** Returns the prototype invariant for MultiplyDouble_yxz **/
  public static /*@Prototype*/ MultiplyDouble_yxz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ MultiplyDouble_yxz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected MultiplyDouble_yxz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new MultiplyDouble_yxz (slice);
  }

  private MultiplyDouble_yxz (PptSlice slice) {
    super (slice);
  }

  public MultiplyDouble_yxz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"", " * ", ""};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert MultiplyDouble_yxz.function_id == -1;
    MultiplyDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (true);
  }

  public double func (double x, double z) {

    return (x * z);
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (y, x, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", y, x, z));
    return (add_ordered (y, x, z, count));
  }

  public boolean isMultiply() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (MultiplyDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(1,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == 0) && (x == 0) ==> r = x * z
        new NISuppression (result_eq_0, arg1_eq_0, suppressee),

        // (r == 0) && (z == 0) ==> r = x * z
        new NISuppression (result_eq_0, arg2_eq_0, suppressee),

        // (r == x) && (z == 1) ==> r = x * z
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),

        // (r == z) && (x == 1) ==> r = x * z
        new NISuppression (result_eq_arg2, arg1_eq_1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>z = Multiply (x, y)</samp>
 * over three double scalars.
 */
public static class MultiplyDouble_zxy extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ MultiplyDouble_zxy proto;

  /** Returns the prototype invariant for MultiplyDouble_zxy **/
  public static /*@Prototype*/ MultiplyDouble_zxy get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ MultiplyDouble_zxy ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected MultiplyDouble_zxy instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new MultiplyDouble_zxy (slice);
  }

  private MultiplyDouble_zxy (PptSlice slice) {
    super (slice);
  }

  public MultiplyDouble_zxy () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"", " * ", ""};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert MultiplyDouble_zxy.function_id == -1;
    MultiplyDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (true);
  }

  public double func (double x, double y) {

    return (x * y);
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (z, x, y, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", z, x, y));
    return (add_ordered (z, x, y, count));
  }

  public boolean isMultiply() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (MultiplyDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(2,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (1, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == 0) && (x == 0) ==> r = x * y
        new NISuppression (result_eq_0, arg1_eq_0, suppressee),

        // (r == 0) && (y == 0) ==> r = x * y
        new NISuppression (result_eq_0, arg2_eq_0, suppressee),

        // (r == x) && (y == 1) ==> r = x * y
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),

        // (r == y) && (x == 1) ==> r = x * y
        new NISuppression (result_eq_arg2, arg1_eq_1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

  // "define" EQUALITY_MIN_MAX_SUPPRESS

  // default is that it is not this function, overriden in the subclass
  public boolean isMinimum () {
    return (false);
  }

/**
 * Represents the invariant <samp>x = Minimum (y, z)</samp>
 * over three double scalars.
 */
public static class MinimumDouble_xyz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ MinimumDouble_xyz proto;

  /** Returns the prototype invariant for MinimumDouble_xyz **/
  public static /*@Prototype*/ MinimumDouble_xyz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ MinimumDouble_xyz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected MinimumDouble_xyz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new MinimumDouble_xyz (slice);
  }

  private MinimumDouble_xyz (PptSlice slice) {
    super (slice);
  }

  public MinimumDouble_xyz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert MinimumDouble_xyz.function_id == -1;
    MinimumDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (true);
  }

  public double func (double y, double z) {

    return (Math.min (y, z));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (x, y, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", x, y, z));
    return (add_ordered (x, y, z, count));
  }

  public boolean isMinimum() {
    return (true);
  }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (MinimumDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(0,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (x == y) && (y <= z) ==> r = min(y, z)
        new NISuppression (result_eq_arg1, arg1_le_arg2, suppressee),

        // (x == z) && (z <= y) ==> r = min(y, z)
        new NISuppression (result_eq_arg2, arg2_le_arg1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>y = Minimum (x, z)</samp>
 * over three double scalars.
 */
public static class MinimumDouble_yxz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ MinimumDouble_yxz proto;

  /** Returns the prototype invariant for MinimumDouble_yxz **/
  public static /*@Prototype*/ MinimumDouble_yxz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ MinimumDouble_yxz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected MinimumDouble_yxz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new MinimumDouble_yxz (slice);
  }

  private MinimumDouble_yxz (PptSlice slice) {
    super (slice);
  }

  public MinimumDouble_yxz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert MinimumDouble_yxz.function_id == -1;
    MinimumDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (true);
  }

  public double func (double x, double z) {

    return (Math.min (x, z));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (y, x, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", y, x, z));
    return (add_ordered (y, x, z, count));
  }

  public boolean isMinimum() {
    return (true);
  }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (MinimumDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(1,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (y == x) && (x <= z) ==> r = min(x, z)
        new NISuppression (result_eq_arg1, arg1_le_arg2, suppressee),

        // (y == z) && (z <= x) ==> r = min(x, z)
        new NISuppression (result_eq_arg2, arg2_le_arg1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>z = Minimum (x, y)</samp>
 * over three double scalars.
 */
public static class MinimumDouble_zxy extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ MinimumDouble_zxy proto;

  /** Returns the prototype invariant for MinimumDouble_zxy **/
  public static /*@Prototype*/ MinimumDouble_zxy get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ MinimumDouble_zxy ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected MinimumDouble_zxy instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new MinimumDouble_zxy (slice);
  }

  private MinimumDouble_zxy (PptSlice slice) {
    super (slice);
  }

  public MinimumDouble_zxy () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.min(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert MinimumDouble_zxy.function_id == -1;
    MinimumDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (true);
  }

  public double func (double x, double y) {

    return (Math.min (x, y));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (z, x, y, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", z, x, y));
    return (add_ordered (z, x, y, count));
  }

  public boolean isMinimum() {
    return (true);
  }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (MinimumDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(2,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (1, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (z == x) && (x <= y) ==> r = min(x, y)
        new NISuppression (result_eq_arg1, arg1_le_arg2, suppressee),

        // (z == y) && (y <= x) ==> r = min(x, y)
        new NISuppression (result_eq_arg2, arg2_le_arg1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

  // "define" EQUALITY_MIN_MAX_SUPPRESS

  // default is that it is not this function, overriden in the subclass
  public boolean isMaximum () {
    return (false);
  }

/**
 * Represents the invariant <samp>x = Maximum (y, z)</samp>
 * over three double scalars.
 */
public static class MaximumDouble_xyz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ MaximumDouble_xyz proto;

  /** Returns the prototype invariant for MaximumDouble_xyz **/
  public static /*@Prototype*/ MaximumDouble_xyz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ MaximumDouble_xyz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected MaximumDouble_xyz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new MaximumDouble_xyz (slice);
  }

  private MaximumDouble_xyz (PptSlice slice) {
    super (slice);
  }

  public MaximumDouble_xyz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert MaximumDouble_xyz.function_id == -1;
    MaximumDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (true);
  }

  public double func (double y, double z) {

    return (Math.max (y, z));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (x, y, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", x, y, z));
    return (add_ordered (x, y, z, count));
  }

  public boolean isMaximum() {
    return (true);
  }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (MaximumDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(0,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == y) && (z <= y) ==> r = max(y, z)
        new NISuppression (result_eq_arg1, arg2_le_arg1, suppressee),

        // (r == z) && (y <= z) ==> r = max(y, z)
        new NISuppression (result_eq_arg2, arg1_le_arg2, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>y = Maximum (x, z)</samp>
 * over three double scalars.
 */
public static class MaximumDouble_yxz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ MaximumDouble_yxz proto;

  /** Returns the prototype invariant for MaximumDouble_yxz **/
  public static /*@Prototype*/ MaximumDouble_yxz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ MaximumDouble_yxz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected MaximumDouble_yxz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new MaximumDouble_yxz (slice);
  }

  private MaximumDouble_yxz (PptSlice slice) {
    super (slice);
  }

  public MaximumDouble_yxz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert MaximumDouble_yxz.function_id == -1;
    MaximumDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (true);
  }

  public double func (double x, double z) {

    return (Math.max (x, z));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (y, x, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", y, x, z));
    return (add_ordered (y, x, z, count));
  }

  public boolean isMaximum() {
    return (true);
  }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (MaximumDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(1,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == x) && (z <= x) ==> r = max(x, z)
        new NISuppression (result_eq_arg1, arg2_le_arg1, suppressee),

        // (r == z) && (x <= z) ==> r = max(x, z)
        new NISuppression (result_eq_arg2, arg1_le_arg2, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>z = Maximum (x, y)</samp>
 * over three double scalars.
 */
public static class MaximumDouble_zxy extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ MaximumDouble_zxy proto;

  /** Returns the prototype invariant for MaximumDouble_zxy **/
  public static /*@Prototype*/ MaximumDouble_zxy get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ MaximumDouble_zxy ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected MaximumDouble_zxy instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new MaximumDouble_zxy (slice);
  }

  private MaximumDouble_zxy (PptSlice slice) {
    super (slice);
  }

  public MaximumDouble_zxy () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.max(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert MaximumDouble_zxy.function_id == -1;
    MaximumDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (true);
  }

  public double func (double x, double y) {

    return (Math.max (x, y));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (z, x, y, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", z, x, y));
    return (add_ordered (z, x, y, count));
  }

  public boolean isMaximum() {
    return (true);
  }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (MaximumDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(2,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (1, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == x) && (y <= x) ==> r = max(x, y)
        new NISuppression (result_eq_arg1, arg2_le_arg1, suppressee),

        // (r == y) && (x <= y) ==> r = max(x, y)
        new NISuppression (result_eq_arg2, arg1_le_arg2, suppressee),

      });

  // Create a suppression factory for functionBinary

}

  // default is that it is not this function, overriden in the subclass
  public boolean isDivision () {
    return (false);
  }

/**
 * Represents the invariant <samp>x = Division (y, z)</samp>
 * over three double scalars.
 */
public static class DivisionDouble_xyz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ DivisionDouble_xyz proto;

  /** Returns the prototype invariant for DivisionDouble_xyz **/
  public static /*@Prototype*/ DivisionDouble_xyz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ DivisionDouble_xyz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected DivisionDouble_xyz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new DivisionDouble_xyz (slice);
  }

  private DivisionDouble_xyz (PptSlice slice) {
    super (slice);
  }

  public DivisionDouble_xyz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert DivisionDouble_xyz.function_id == -1;
    DivisionDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double y, double z) {

    return ((y / z));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (x, y, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", x, y, z));
    return (add_ordered (x, y, z, count));
  }

  public boolean isDivision() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (DivisionDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(0,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (y == z) && (z != 0) && (r == 1)
        new NISuppression (arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

        // (r == y) && (z == 1) ==> r = y / z
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),
      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>y = Division (x, z)</samp>
 * over three double scalars.
 */
public static class DivisionDouble_yxz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ DivisionDouble_yxz proto;

  /** Returns the prototype invariant for DivisionDouble_yxz **/
  public static /*@Prototype*/ DivisionDouble_yxz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ DivisionDouble_yxz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected DivisionDouble_yxz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new DivisionDouble_yxz (slice);
  }

  private DivisionDouble_yxz (PptSlice slice) {
    super (slice);
  }

  public DivisionDouble_yxz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert DivisionDouble_yxz.function_id == -1;
    DivisionDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double x, double z) {

    return ((x / z));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (y, x, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", y, x, z));
    return (add_ordered (y, x, z, count));
  }

  public boolean isDivision() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (DivisionDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(1,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (x == z) && (z != 0) && (r == 1)
        new NISuppression (arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

        // (r == x) && (z == 1) ==> r = x / z
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),
      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>z = Division (x, y)</samp>
 * over three double scalars.
 */
public static class DivisionDouble_zxy extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ DivisionDouble_zxy proto;

  /** Returns the prototype invariant for DivisionDouble_zxy **/
  public static /*@Prototype*/ DivisionDouble_zxy get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ DivisionDouble_zxy ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected DivisionDouble_zxy instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new DivisionDouble_zxy (slice);
  }

  private DivisionDouble_zxy (PptSlice slice) {
    super (slice);
  }

  public DivisionDouble_zxy () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert DivisionDouble_zxy.function_id == -1;
    DivisionDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double x, double y) {

    return ((x / y));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (z, x, y, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", z, x, y));
    return (add_ordered (z, x, y, count));
  }

  public boolean isDivision() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (DivisionDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(2,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (1, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (x == y) && (y != 0) && (r == 1)
        new NISuppression (arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

        // (r == x) && (y == 1) ==> r = x / y
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),
      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>x = Division (z, y)</samp>
 * over three double scalars.
 */
public static class DivisionDouble_xzy extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ DivisionDouble_xzy proto;

  /** Returns the prototype invariant for DivisionDouble_xzy **/
  public static /*@Prototype*/ DivisionDouble_xzy get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ DivisionDouble_xzy ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected DivisionDouble_xzy instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new DivisionDouble_xzy (slice);
  }

  private DivisionDouble_xzy (PptSlice slice) {
    super (slice);
  }

  public DivisionDouble_xzy () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert DivisionDouble_xzy.function_id == -1;
    DivisionDouble_xzy.function_id = function_id;
  }

  private static int var_order = 4;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double z, double y) {

    return ((z / y));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (x, z, y, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", x, z, y));
    return (add_ordered (x, z, y, count));
  }

  public boolean isDivision() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (DivisionDouble_xzy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (0, 2, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (0, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (2, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (2, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (1, 2, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (2, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (1, 2, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(0,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (1, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (z == y) && (y != 0) && (r == 1)
        new NISuppression (arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

        // (r == z) && (y == 1) ==> r = z / y
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),
      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>y = Division (z, x)</samp>
 * over three double scalars.
 */
public static class DivisionDouble_yzx extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ DivisionDouble_yzx proto;

  /** Returns the prototype invariant for DivisionDouble_yzx **/
  public static /*@Prototype*/ DivisionDouble_yzx get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ DivisionDouble_yzx ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected DivisionDouble_yzx instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new DivisionDouble_yzx (slice);
  }

  private DivisionDouble_yzx (PptSlice slice) {
    super (slice);
  }

  public DivisionDouble_yzx () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert DivisionDouble_yzx.function_id == -1;
    DivisionDouble_yzx.function_id = function_id;
  }

  private static int var_order = 5;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double z, double x) {

    return ((z / x));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (y, z, x, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", y, z, x));
    return (add_ordered (y, z, x, count));
  }

  public boolean isDivision() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (DivisionDouble_yzx.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (1, 2, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (1, 0, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (2, 0, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (1, 0, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (2, 0, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (0, 2, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (1, 0, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (2, 0, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (0, 2, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(1,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (0, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (z == x) && (x != 0) && (r == 1)
        new NISuppression (arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

        // (r == z) && (x == 1) ==> r = z / x
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),
      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>z = Division (y, x)</samp>
 * over three double scalars.
 */
public static class DivisionDouble_zyx extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ DivisionDouble_zyx proto;

  /** Returns the prototype invariant for DivisionDouble_zyx **/
  public static /*@Prototype*/ DivisionDouble_zyx get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ DivisionDouble_zyx ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected DivisionDouble_zyx instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new DivisionDouble_zyx (slice);
  }

  private DivisionDouble_zyx (PptSlice slice) {
    super (slice);
  }

  public DivisionDouble_zyx () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"", " / ", ""};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert DivisionDouble_zyx.function_id == -1;
    DivisionDouble_zyx.function_id = function_id;
  }

  private static int var_order = 6;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double y, double x) {

    return ((y / x));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (z, y, x, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", z, y, x));
    return (add_ordered (z, y, x, count));
  }

  public boolean isDivision() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (DivisionDouble_zyx.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (2, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (2, 0, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (1, 0, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (2, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (2, 0, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (1, 0, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (0, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (2, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (2, 0, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (1, 0, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (0, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(2,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (0, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (y == x) && (x != 0) && (r == 1)
        new NISuppression (arg1_eq_arg2, arg2_ne_0, result_eq_1, suppressee),

        // (r == y) && (x == 1) ==> r = y / x
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),
      });

  // Create a suppression factory for functionBinary

}

  // default is that it is not this function, overriden in the subclass
  public boolean isPower () {
    return (false);
  }

/**
 * Represents the invariant <samp>x = Power (y, z)</samp>
 * over three double scalars.
 */
public static class PowerDouble_xyz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ PowerDouble_xyz proto;

  /** Returns the prototype invariant for PowerDouble_xyz **/
  public static /*@Prototype*/ PowerDouble_xyz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ PowerDouble_xyz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected PowerDouble_xyz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new PowerDouble_xyz (slice);
  }

  private PowerDouble_xyz (PptSlice slice) {
    super (slice);
  }

  public PowerDouble_xyz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert PowerDouble_xyz.function_id == -1;
    PowerDouble_xyz.function_id = function_id;
  }

  private static int var_order = 1;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double y, double z) {

    return (Math.pow (y, z));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (x, y, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", x, y, z));
    return (add_ordered (x, y, z, count));
  }

  public boolean isPower() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (PowerDouble_xyz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (0, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(0,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit z to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == 1) && (z == 0) ==> r = pow (y, z)
        new NISuppression (result_eq_1, arg2_eq_0, suppressee),

        // (r == 1) && (y == 1) && (z >= 0)   ==> r = pow (y, z)
        new NISuppression (result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

        // (r == 0) && (y == 0) && (z > 0)
        new NISuppression (result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                          suppressee),

        // (r == y) && (z == 1)    ==> r = pow (y, z)
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>y = Power (x, z)</samp>
 * over three double scalars.
 */
public static class PowerDouble_yxz extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ PowerDouble_yxz proto;

  /** Returns the prototype invariant for PowerDouble_yxz **/
  public static /*@Prototype*/ PowerDouble_yxz get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ PowerDouble_yxz ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected PowerDouble_yxz instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new PowerDouble_yxz (slice);
  }

  private PowerDouble_yxz (PptSlice slice) {
    super (slice);
  }

  public PowerDouble_yxz () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert PowerDouble_yxz.function_id == -1;
    PowerDouble_yxz.function_id = function_id;
  }

  private static int var_order = 2;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double x, double z) {

    return (Math.pow (x, z));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (y, x, z, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", y, x, z));
    return (add_ordered (y, x, z, count));
  }

  public boolean isPower() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (PowerDouble_yxz.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (1, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (1, 2, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 2, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(1,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (2, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit z to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == 1) && (z == 0) ==> r = pow (x, z)
        new NISuppression (result_eq_1, arg2_eq_0, suppressee),

        // (r == 1) && (x == 1) && (z >= 0)   ==> r = pow (x, z)
        new NISuppression (result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

        // (r == 0) && (x == 0) && (z > 0)
        new NISuppression (result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                          suppressee),

        // (r == x) && (z == 1)    ==> r = pow (x, z)
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>z = Power (x, y)</samp>
 * over three double scalars.
 */
public static class PowerDouble_zxy extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ PowerDouble_zxy proto;

  /** Returns the prototype invariant for PowerDouble_zxy **/
  public static /*@Prototype*/ PowerDouble_zxy get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ PowerDouble_zxy ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected PowerDouble_zxy instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new PowerDouble_zxy (slice);
  }

  private PowerDouble_zxy (PptSlice slice) {
    super (slice);
  }

  public PowerDouble_zxy () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert PowerDouble_zxy.function_id == -1;
    PowerDouble_zxy.function_id = function_id;
  }

  private static int var_order = 3;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double x, double y) {

    return (Math.pow (x, y));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (z, x, y, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", z, x, y));
    return (add_ordered (z, x, y, count));
  }

  public boolean isPower() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (PowerDouble_zxy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (2, 0, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (2, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (0, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (2, 0, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (2, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (1, 0, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (2, 0, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (2, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (1, 0, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(2,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (1, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit y to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == 1) && (y == 0) ==> r = pow (x, y)
        new NISuppression (result_eq_1, arg2_eq_0, suppressee),

        // (r == 1) && (x == 1) && (y >= 0)   ==> r = pow (x, y)
        new NISuppression (result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

        // (r == 0) && (x == 0) && (y > 0)
        new NISuppression (result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                          suppressee),

        // (r == x) && (y == 1)    ==> r = pow (x, y)
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>x = Power (z, y)</samp>
 * over three double scalars.
 */
public static class PowerDouble_xzy extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ PowerDouble_xzy proto;

  /** Returns the prototype invariant for PowerDouble_xzy **/
  public static /*@Prototype*/ PowerDouble_xzy get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ PowerDouble_xzy ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected PowerDouble_xzy instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new PowerDouble_xzy (slice);
  }

  private PowerDouble_xzy (PptSlice slice) {
    super (slice);
  }

  public PowerDouble_xzy () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert PowerDouble_xzy.function_id == -1;
    PowerDouble_xzy.function_id = function_id;
  }

  private static int var_order = 4;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double z, double y) {

    return (Math.pow (z, y));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (x, z, y, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", x, z, y));
    return (add_ordered (x, z, y, count));
  }

  public boolean isPower() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (PowerDouble_xzy.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (0, 2, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (0, 1, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (2, 1, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (0, 2, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (0, 1, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (2, 1, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (1, 2, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (0, 2, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (0, 1, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (2, 1, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (1, 2, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(0, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(0,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (0, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (1, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit y to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == 1) && (y == 0) ==> r = pow (z, y)
        new NISuppression (result_eq_1, arg2_eq_0, suppressee),

        // (r == 1) && (z == 1) && (y >= 0)   ==> r = pow (z, y)
        new NISuppression (result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

        // (r == 0) && (z == 0) && (y > 0)
        new NISuppression (result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                          suppressee),

        // (r == z) && (y == 1)    ==> r = pow (z, y)
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>y = Power (z, x)</samp>
 * over three double scalars.
 */
public static class PowerDouble_yzx extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ PowerDouble_yzx proto;

  /** Returns the prototype invariant for PowerDouble_yzx **/
  public static /*@Prototype*/ PowerDouble_yzx get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ PowerDouble_yzx ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected PowerDouble_yzx instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new PowerDouble_yzx (slice);
  }

  private PowerDouble_yzx (PptSlice slice) {
    super (slice);
  }

  public PowerDouble_yzx () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert PowerDouble_yzx.function_id == -1;
    PowerDouble_yzx.function_id = function_id;
  }

  private static int var_order = 5;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double z, double x) {

    return (Math.pow (z, x));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (y, z, x, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", y, z, x));
    return (add_ordered (y, z, x, count));
  }

  public boolean isPower() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (PowerDouble_yzx.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (1, 2, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (1, 0, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (2, 0, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (1, 2, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (1, 0, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (2, 0, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (0, 2, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (1, 2, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (1, 0, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (2, 0, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (0, 2, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(1, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (2, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(1,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (2, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (0, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit x to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == 1) && (x == 0) ==> r = pow (z, x)
        new NISuppression (result_eq_1, arg2_eq_0, suppressee),

        // (r == 1) && (z == 1) && (x >= 0)   ==> r = pow (z, x)
        new NISuppression (result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

        // (r == 0) && (z == 0) && (x > 0)
        new NISuppression (result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                          suppressee),

        // (r == z) && (x == 1)    ==> r = pow (z, x)
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

/**
 * Represents the invariant <samp>z = Power (y, x)</samp>
 * over three double scalars.
 */
public static class PowerDouble_zyx extends FunctionBinaryFloat {
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20031030L;

  private static /*@Prototype*/ PowerDouble_zyx proto;

  /** Returns the prototype invariant for PowerDouble_zyx **/
  public static /*@Prototype*/ PowerDouble_zyx get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ PowerDouble_zyx ();
    return (proto);
  }

  /** instantiate an invariant on the specified slice **/
  protected PowerDouble_zyx instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new PowerDouble_zyx (slice);
  }

  private PowerDouble_zyx (PptSlice slice) {
    super (slice);
  }

  public PowerDouble_zyx () /*@Prototype*/ {
    super ();
  }

  private static String[] method_name = new String[] {"java.lang.Math.pow(", ", ", ")"};

  public String[] get_method_name () {
    return (method_name);
  }

  private static int function_id = -1;

  public int get_function_id() {
    return (function_id);
  }

  public void set_function_id (int function_id) {
    assert PowerDouble_zyx.function_id == -1;
    PowerDouble_zyx.function_id = function_id;
  }

  private static int var_order = 6;

  public int get_var_order() {
    return var_order;
  }

  public boolean is_symmetric() {

      return (false);
  }

  public double func (double y, double x) {

    return (Math.pow (y, x));
  }

  public InvariantStatus check_modified(double x, double y,
                                      double z, int count) {
    return (check_ordered (z, y, x, count));
  }

  public InvariantStatus add_modified(double x, double y,
                                      double z, int count) {
    if (Debug.logDetail())
      log (String.format ("result=%s, arg1=%s, arg2=%s", z, y, x));
    return (add_ordered (z, y, x, count));
  }

  public boolean isPower() {
    return (true);
  }

    public boolean isExact() { return true; }

  /**
   * Returns a list of non-instantiating suppressions for this invariant.
   */
  public /*@Nullable*/ NISuppressionSet get_ni_suppressions() {
    if (NIS.dkconfig_enabled && dkconfig_enabled)
      return (suppressions);
    else
      return (null);
  }

  /** definition of this invariant (the suppressee) **/
  private static NISuppressee suppressee
                    = new NISuppressee (PowerDouble_zyx.class, 3);

  // suppressor definitions (used below)
  private static NISuppressor result_eq_arg1
    = new NISuppressor (2, 1, FloatEqual.class);
  private static NISuppressor result_eq_arg2
    = new NISuppressor (2, 0, FloatEqual.class);
  private static NISuppressor arg1_eq_arg2
    = new NISuppressor (1, 0, FloatEqual.class);

  private static NISuppressor result_lt_arg1
    = new NISuppressor (2, 1, FloatLessThan.class);
  private static NISuppressor result_lt_arg2
    = new NISuppressor (2, 0, FloatLessThan.class);
  private static NISuppressor arg1_lt_arg2
    = new NISuppressor (1, 0, FloatLessThan.class);
  private static NISuppressor arg2_lt_arg1
    = new NISuppressor (0, 1, FloatLessThan.class);

  private static NISuppressor result_le_arg1
    = new NISuppressor (2, 1, FloatLessEqual.class);
  private static NISuppressor result_le_arg2
    = new NISuppressor (2, 0, FloatLessEqual.class);
  private static NISuppressor arg1_le_arg2
    = new NISuppressor (1, 0, FloatLessEqual.class);
  private static NISuppressor arg2_le_arg1
    = new NISuppressor (0, 1, FloatLessEqual.class);

  private static NISuppressor result_track0_arg1
    = new NISuppressor (2, 1, NumericInt.ZeroTrack.class);
  private static NISuppressor result_track0_arg2
    = new NISuppressor (2, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_arg2
    = new NISuppressor (1, 0, NumericInt.ZeroTrack.class);
  private static NISuppressor arg1_track0_result
    = new NISuppressor (1, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_result
    = new NISuppressor (0, 2, NumericInt.ZeroTrack.class);
  private static NISuppressor arg2_track0_arg1
    = new NISuppressor (0, 1, NumericInt.ZeroTrack.class);

  private static NISuppressor result_eq_1
    = new NISuppressor(2, RangeFloat.EqualOne.class);
  private static NISuppressor arg1_eq_1
    = new NISuppressor (1, RangeFloat.EqualOne.class);
  private static NISuppressor arg2_eq_1
    = new NISuppressor (0, RangeFloat.EqualOne.class);

  private static NISuppressor result_eq_0
    = new NISuppressor(2,RangeFloat.EqualZero.class);
  private static NISuppressor arg1_eq_0
    = new NISuppressor (1, RangeFloat.EqualZero.class);
  private static NISuppressor arg2_eq_0
    = new NISuppressor (0, RangeFloat.EqualZero.class);

  private static NISuppressor result_ne_0
    = new NISuppressor (2, NonZeroFloat.class);
  private static NISuppressor arg1_ne_0
    = new NISuppressor (1, NonZeroFloat.class);
  private static NISuppressor arg2_ne_0
    = new NISuppressor (0, NonZeroFloat.class);

  private static NISuppressor result_ge_0
    = new NISuppressor (2, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg1_ge_0
    = new NISuppressor (1, RangeFloat.GreaterEqualZero.class);
  private static NISuppressor arg2_ge_0
    = new NISuppressor (0, RangeFloat.GreaterEqualZero.class);

  private static NISuppressor result_ge_64
    = new NISuppressor (2, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg1_ge_64
    = new NISuppressor (1, RangeInt.GreaterEqual64.class);
  private static NISuppressor arg2_ge_64
    = new NISuppressor (0, RangeInt.GreaterEqual64.class);

    // Note that any suppression that doesn't limit x to valid exponents
    // (>= 0), must check for valid exponents as well (so that the invariant
    // is correctly destroyed on invalid exponents)
    //
    // Note also that pow(0,0) == 1 and pow(0,x), where (x > 0), == 0
    // Another interesting artificat of pow is that for any even base, any
    // exponent >= 64 will yield a result of 0.  For example, pow(10,256) == 0
    // (at least for integers)

    private static NISuppressionSet suppressions
      = new NISuppressionSet (new NISuppression[] {

        // (r == 1) && (x == 0) ==> r = pow (y, x)
        new NISuppression (result_eq_1, arg2_eq_0, suppressee),

        // (r == 1) && (y == 1) && (x >= 0)   ==> r = pow (y, x)
        new NISuppression (result_eq_1, arg1_eq_1, arg2_ge_0, suppressee),

        // (r == 0) && (y == 0) && (x > 0)
        new NISuppression (result_eq_0, arg1_eq_0, arg2_ne_0, arg2_ge_0,
                          suppressee),

        // (r == y) && (x == 1)    ==> r = pow (y, x)
        new NISuppression (result_eq_arg1, arg2_eq_1, suppressee),

      });

  // Create a suppression factory for functionBinary

}

}
